package ch.epfl.lara.matcheck;

import ch.epfl.lara.matcheck.tester.TesterSkeleton
import ch.epfl.lara.matcheck.util.statistics.TreeStatistic

object matcheck extends TesterSkeleton {

  import Constants.{CONFIG_SUFFIX,SCALA_SUFFIX}
  
  def main(args: Array[String]) {
    Timer.start()
    var tree_stats: TreeStatistic = null
    var report_msg_error: String = null
    var conf_filename: String = null
    var scala_filename: String = null
    var options: List[String] = Nil
    
    var continue = true
    for(arg<-args if continue) {
      if(arg.endsWith(CONFIG_SUFFIX)) {
        if(conf_filename == null) conf_filename = arg
        else {
          report_msg_error = "matcheck: error: don't know what to do with more than one '*.conf' config file"
          continue = false
        }
      } else if (arg.endsWith(SCALA_SUFFIX)) { 
        if (scala_filename == null)
          scala_filename = arg
        else {
          report_msg_error = "matcheck: error: don't know what to do with more than one '*.scala' source file"
          continue = false
        }
      }else if(arg.startsWith("-")) 
        Options(arg)
      else {
        report_msg_error = "matcheck: error: don't know what to do with "+arg
        continue = false
      }
    }
    
    if(report_msg_error != null) {
      Report.cleanFail(report_msg_error)
    }
    
    
    if(scala_filename == null || 
       conf_filename == null  ||
       Config.HELP) {
       ch.epfl.lara.matcheck.util.printer.MatcheckUsagePrinter.apply
       return ()
    }
    else { 
      Report.verbose("Parsing configuration file '"+conf_filename+"'")
      new ConfigParser(conf_filename).parse
      
      Config.verbose
      
      val program = ParsePhase(scala_filename)    // parse the source scala file
      
      tree_stats = new TreeStatistic(program)

      Timer.finishedParsing()
      
      NameAnalyzePhase(program)                   // check semantic of the program
      val desugared = DesugarPhase(program)
      NameAnalyzePhase(desugared)                   // check semantic of the program
      val fresh_program = FreshTreePhase(desugared) // generate fresh names for each identifier
      if(!Config.NOCHECKS) {
        verifyConfig
        VerifyPhase(fresh_program)
        Timer.stop()
        if(Config.PERFORMANCE) Timer.verbose()
      }
      else {
        Report.verbose("\nOption -nochecks enabled. The parsed source is printed.")
        ch.epfl.lara.matcheck.util.printer.PrettyPrinterTree(fresh_program)
        Timer.stop()
        if(Config.PERFORMANCE) Timer.verbose()
      }
    }
    tree_stats.verbose()
  }
  
  
  
  private def verifyConfig {
    if(!Config.PROVER())
      Report.cleanFail("Prover '"+Config.PROVER_EXEC+"' can't be executed. Check your config file "+
        	  "and verify that '"+Config.PROVER_EXEC+"' is in your path.")
  }
  
  
  import scala.util.parsing.input.{StreamReader,Reader}
  import java.io.{InputStreamReader,File,FileInputStream,StringReader}
  import ch.epfl.lara.matcheck.verify.provers.TheoremProvers
  class ConfigParser {
    
    private var in: Reader[Char] = _
    
    
    def this(in: Reader[Char]) = {
      this()
      this. in = in
      readCh() // initializes
    }
    
    def this(file: File) = {
      this(StreamReader(new InputStreamReader(new FileInputStream(file),"ISO-8859-1")))
    }
    
    def this(fileName: String) = {
      this(new File(fileName))
    }
    
    private val reserved = List("proverName", "proverExec", "proverOptions")
    
    private var ch: Char = _
    
    
    
    private def readCh() { 
      ch = in.first
      in = in.rest
    }
    
    
    
    private def parse(f: Char => Boolean) {
      while(f(ch) && !in.atEnd)
        readCh()
    }
    
    
    private def parseSpaces() {
      parse(x => Character.isSpaceChar(x))
    }
    
    private def parseWhitespaces() {
      parse(x => Character.isWhitespace(x))
    }
    
    private def parseToken(token: String) {
      parseSpaces()
      for(i<-List.range(0,token.length)) {
        if(in.atEnd) error("expected '"+token.charAt(i)+"', found <eof>")
        if (ch != token.charAt(i)) error("expected '"+token.charAt(i)+"', found '"+ch+"'")
        readCh()
      }
    }
    
    
    private def read(): String = {
      val buf = new StringBuffer
      
      while(ch != Character.LINE_SEPARATOR && ch != '\n' && !in.atEnd) {
        buf.append(ch)
        readCh()
      }
      if(!in.atEnd) readCh()
      buf.toString
    }
    
    private def readLine(token: String): String = {
      parseToken(token)
      parseToken(":")
      read()
    }
    
    
    def parse {
      for(token<-reserved) {
        val line = readLine(token)
        token match {
          case "proverName"    => Config.PROVER = getProver(line.trim());
          case "proverExec"    => Config.PROVER_EXEC = line.trim()
          case "proverOptions" => Config.PROVER_OPTIONS = line
          case _               => error("don't know what to do with '"+token+"'")
        }
      }
      parseWhitespaces()
      if(!in.atEnd) error("expected <eof>, found '"+ch+"'")
    }
    

    
    private def getProver(name: String): TheoremProvers.Prover =
      TheoremProvers.string2prover(name)
  }
  
  
 
  
}
	